Zipper as Insecticide

From the 2005 ACM SIGPLAN Workshop on ML, here is An Applicative Control-Flow Graph Based on Huet's Zipper, by Norman Ramsey and João Dias.

We are using ML to build a compiler that does low-level optimization. To support optimizations in classic imperative style, we built a control-flow graph using mutable pointers and other mutable state in the nodes. This decision proved unfortunate: the mutable flow graph was big and complex, it led to many bugs. We have replaced it by a smaller, simpler, applicative flow graph based on Huet's (1997) zipper. The new flow graph is a success; this paper presents its design and shows how it leads to a gratifyingly simple implementation of the dataflow framework developed by Lerner, Grove, and Chambers (2002).

Jon Udell on CoScripter

The web site description of CoScripter:

CoScripter is a system for recording, automating, and sharing processes performed in a web browser such as printing photos online, requesting a vacation hold for postal mail, or checking bank account information. Instructions for processes are recorded and stored in easy-to-read text here on the CoScripter web site, so anyone can make use of them. If you are having trouble with a web-based process, check to see if someone has written a CoScript for it!

Jon's discussion emphasizes the DSL perspective (and end-user programming).

The community dynamics enabled by exposing a DSL seem to me the interesting aspect of this discussion. Yet another example you can use when arguing in favor of textual, user accessible, DSLs.

Squeak by Example

Squeak by Example is an open-source book about Squeak. Squeak is an open-source implementation of the Smalltalk-80 programming language and environment...

A first version of the book is planned to be released mid-September, 2007. The book will be available for free download as PDF. We will also offer the possibility to order a print-on-demand copy. The complete LaTeX sources will also be available for download.

You can browse the LaTex files in the svn repository.

Tagless Staged Interpreters for Simpler Typed Languages

Finally Tagless, Partially Evaluated, Tagless Staged Interpreters for Simpler Typed Languages.
Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.

We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value CPS transformers.
Our main idea is to encode HOAS using cogen functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the LC. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations.

Oleg explains:

It seems like a common wisdom that an embedding of a typed object language (e.g., DSL) to a typed meta-language so that all and only typed object terms can be represented requires dependent types, GADTs or other such advanced type systems. In fact, this problem of writing (tagless) type-preserving typed interpreters has been the motivation for most of the papers on GADTs. We show that regardless of merits and conveniences of GADTs, type-preserving typed interpretation can be achieved with no GADTs whatsoever, using very simple type systems of ML or Haskell98. We also show the same approach lets us perform statically type-preserving partial evaluation and call-by-value or call-by-name CPS tansformations. The latter transformations, too, are often claimed impossible in Haskell98 or ML - requiring instead quite advanced type systems or language features.

The complete (Meta)OCaml and Haskell code accompanying the paper is
available (see readme).

One of features of our approach is writing the DSL code in a form that can be interpreted in multiple ways. Recently we have become aware the very same approach underlies `abstract categorial grammars' (ACG) in linguistics. Chung-chieh Shan has written an extensive article on this correspondence. That post itself can be interpreted in several ways: the file can be read as plain text, or it can be loaded as it is in Haskell or OCaml interpreters.

It should be noted that the linguistic terms `tectogrammatics' and `phenogrammatics' were coined by none else but Haskell Curry, in his famous 1961 paper 'Some Logical Aspects of Grammatical Structure'. The summary of the ESSLLI workshop describes further connections to linear lambda-calculus.

The paper has been accepted for APLAS; the authors appreciate any comments indeed.

No Name: Just Notes on Software Reuse

No Name: Just Notes on Software Reuse. Robert Biddle, Angela Martin, James Noble.

In the beginning, so our myths and stories tell us, the programmer created the program from the eternal nothingness of the void. In this essay, we recognise that programs these days are like any other assemblage, and suggest that in fact programming has always been about reuse. We also explore the nature of reuse, and claim that Components themselves are not the most important consideration for reuse; it is the end product, the composition. The issues still involve value, investment, and return. But pervasive reuse promotes a change in the method of construction of the program, and in the program itself.

This report isn't new, but seeing as it's awfully quiet around here and it does contain amusing pictures and quotations, I thought I'd share the link.

Escape from Zurg: An Exercise in Logic Programming

Escape from Zurg: An Exercise in Logic Programming by Martin Erwig. Journal of Functional Programming, Vol. 14, No. 3, 253-261, 2004

In this article we will illustrate with an example that modern functional programming languages like Haskell can be used effectively for programming search problems, in contrast to the widespread belief that Prolog is much better suited for tasks like these.

...

The example that we want to consider is a homework problem that we have given in a graduate level course on programming languages. The problem was one of several exercises to practice programming in Prolog. After observing that many students had problems manipulating term structures in Prolog (after already having learned to use data types in Haskell) and spending a lot of time on debugging, the question arose whether it would be as difficult to develop a solution for this problem in Haskell. This programming exercise worked well, and we report the result in this paper.

(Haskell source code)

Lifting Abstract Interpreters to Quantified Logical Domains

Lifting Abstract Interpreters to Quantified Logical Domains. Sumit Gulwani, Bill McCloskey, Ashish Tiwari. July 2007.

Today, abstract interpretation is capable of inferring a wide variety of quantifier-free program invariants. In this paper, we describe a general technique for building powerful quantified abstract domains that leverage existing quantifier-free domains. For example, from a domain that abstracts facts like "a[1] = 0", we automatically construct a domain that can represent universally quantified facts like "Forall i: (0 <= i < n) => A[i]=0)". The principal challenge in building such a domain is that, while most domains supply over-approximations of operations like join, meet, and variable elimination, working with the guards of quantified facts requires under-approximation...

Using our generic construction, we build a number of abstract interpreters on top of domains for linear arithmetic, uninterpreted function symbols (used to model heap accesses), and pointer reachability. Our experiments on a variety of programs using arrays and pointers (including several sorting algorithms) demonstrate the feasibility of the approach on challenging examples.

Barker & Szabolcsi: New directions for proof theory in linguistics

Barker & Szabolcsi: New directions for proof theory in linguistics. ESSLLI 2007.

We sometimes mention that some of the theoretical tools used in PLT are aslo used in linguistics, and this is a great resource for those who want to catch up on recent developments, as well as for those who want to know what's all the fuss is about.

You'll find all the usual suspects: types, continuations, Curry-Howard etc.

Enjoy!

R6RS Validated

R6RS has been ratified, with approximately 2/3rds of voters in favour.